perm filename MARS2[1,JRA] blob
sn#005803 filedate 1972-08-25 generic text, type T, neo UTF8
00100 LE(X1 X2) ↔ R(D(X1 X2)O) ;
00200 LE(D(X1 X2) X1);
00300 LE( D(D(X1 X3) D(X2 X3)) D(D(X1 X2) X3) );
00400 LE(O X1);
00500 R(X1 X1);
00600 (LE(X1 X2) ∧ LE(X2 X1)) → R(X1 X2);
00700 ;
00800
01000 ∀(X1 X2 X3)( LE( X1 X2) ∧ LE( X2 X3)) → LE( X1 X3);
01100 ∀(X1 X2 X3)(LE(D(X1 X2) X3) → LE(D(X1 X3 ) X2));
01200 ∀(X1 X2 X3)(LE(X1 X2) → LE(D(X3 X2) D(X3 X1)));
01250
01300
01400 ∀(X1)R(D(X1 O) X1);;
01500
01550 ∀(X1)R(D(U X1) D(D(U X1) D(U D(U X1))));;
01600
01700